T2: Reasoning about Programs with Type Isomorphisms
We say two types are isomorphic if we can translate from one to the other and back without loss of information. Type isomorphism explain why we can write the same program in many different ways: For example, we can change the order of arguments a function takes, or we can split a function that takes a Boolean argument into two functions. Type isomorphisms allow us to explain why these refactorings don't change the meaning of the program.
The fact that the same program can be written in many different ways, with different types, is convenient for the programmer but makes reasoning and writing tooling more difficult. For this seminar topic, you'll therefore look at a paper (see References) that describes a normal form for types, meaning they present a procedure that translate types into a more uniform shape, so that many isomorphic types become in fact identical.
First, for the programming aspect of the seminar, you will implement the type normalization algorithm from the paper. Then, for the paper, you will explain the work below and briefly discuss applications of type isomorphisms.